/******************************************/
/* DTD Inquisitor 2                       */
/* Copyright: University of Pennsylvania  */
/* Author: Byron Choi                     */
/* Date: 9/2001                           */
/* Contact: kkchoi@gradient.cis.upenn.edu */
/******************************************/
package automata;

import java.util.Hashtable;
import java.util.Iterator;
import java.util.Set;


/**
 * This class represents a Finite State Automata
 * The example bellow demonstrates how the attributes
 * are used in the class
 * 
 * Automata
 * 
 * |1|  A  |2|  B  ||3||
 *     -->     -->
 * alphabet = {A,B}
 * start_state = {1}
 * states = {1,2,3}
 * final_states = {3}
 * t = 1 -> A -> {2}
 *     2 -> B -> {3}
 */

@SuppressWarnings("unchecked")
public class Fsa implements Cloneable {
	private Alphabet alphabet;
	private State start_state;
	private StateSet states;
	private StateSet final_states;
	private Transitions t;
	private State next_unused_state = null;

	/* get a fresh copy of fsa */
	public Fsa() {
		alphabet = new Alphabet();
		states = new StateSet();
		final_states = new StateSet();
		t = new Transitions();
	}

	/* accessor, contructor functions for alphabet of an automata */
	public Alphabet get_alphabet() {
		return alphabet;
	}

	public void add_label(Label l) {
		alphabet.add(l);
	}

	public void add_all_label(Alphabet a) {
		Iterator<Label> i = a.iterator();
		while (i.hasNext()) {
			alphabet.add(i.next());
		}
	}

	public void set_alphabet(Alphabet a) {
		alphabet = a;
	}

	/* accessor, constructor functions for state of an automata */
	public StateSet get_states() {
		return states;
	}

	public State get_start_state() {
		return start_state;
	}

	public StateSet get_final_states() {
		return final_states;
	}

	public void add_state(State s) {
		update_unused_state(s);
		states.add(s);
	}

	public void set_states(StateSet ss) {
		states = ss;
	}

	public void update_unused_state(State s) {
		if (next_unused_state == null) {
			next_unused_state = new State(s.elt.intValue() + 1);
		} else if (next_unused_state.elt.intValue() <= s.elt.intValue()) {
			next_unused_state = new State(s.elt.intValue() + 1);
		}
	}

	public State get_next_unused_state() {
		return next_unused_state;
	}

	public void set_next_unused_state(State s) {
		next_unused_state = s;
	}

	public void set_start_state(State s) {
		add_state(s);
		start_state = s;
	}

	public void set_final_states(StateSet ss) {
		final_states = StateSet.empty();
		Iterator<State> i = ss.iterator();
		while (i.hasNext()) {
			State s = (State) (i.next());
			add_state(s);
			final_states.add(s);
		}
	}

	/* accessor, constructors of transition for an automata */
	public Transitions get_transitions() {
		return t;
	}

	public Alphabet get_labels_of_state(State s) {
		try {
			Alphabet res = new Alphabet();
			Set set = ((Hashtable) (t.get(s))).keySet();
			Iterator i = set.iterator();
			while (i.hasNext()) {
				res.add((Label) (i.next()));
			}
			return res;
		} catch (NullPointerException e) {
			return null;
		}
	}

	public void set_transitions(Transitions t) {
		this.t = t;
	}

	public StateSet get_dest_states(State s) {
		try {
			java.util.Enumeration all = ((Hashtable) (t.get(s))).elements();
			StateSet dest = StateSet.empty();
			while (all.hasMoreElements()) {
				dest = StateSet.union(dest, (StateSet) (all.nextElement()));
			}
			return dest;
		} catch (NullPointerException e) {
			return null;
		}
	}

	public StateSet get_dest_states(State s, Label l) {
		try {
			return (StateSet) (((Hashtable) (t.get(s))).get(l));
		} catch (NullPointerException e) {
			return null;
		}
	}

	public void add_transition(State s, Label l, State d) {
		add_state(s);
		add_state(d);
		add_label(l);

		Hashtable labeltoStateSet = (Hashtable) (t.get(s));
		if (labeltoStateSet == null) {
			labeltoStateSet = new Hashtable();
			labeltoStateSet.put(l, StateSet.singleton(d));
			t.put(s, labeltoStateSet);
		} else {
			StateSet dests = (StateSet) (labeltoStateSet.get(l));
			if (dests == null) {
				labeltoStateSet.put(l, StateSet.singleton(d));
				t.put(s, labeltoStateSet);
			} else {
				dests.add(d);
				labeltoStateSet.put(l, dests);
				t.put(s, labeltoStateSet);
			}
		}
	}

	public boolean is_deterministic() {
		boolean det = true;
		java.util.Iterator i = states.iterator();
		while (i.hasNext() && det) {
			State s = (State) (i.next());
			Alphabet a = get_labels_of_state(s);
			if (a != null) {
				java.util.Iterator i2 = a.iterator();
				while (i2.hasNext() && det) {
					StateSet dests = get_dest_states(s, (Label) (i2.next()));
					if (dests != null) {
						if (dests.size() > 1) {
							det = false;
						}
					}
				}
			}
		}
		return det;
	}

	public Object clone() {
		Fsa fsa = new Fsa();
		fsa.set_alphabet((Alphabet) (this.get_alphabet().clone()));
		fsa.set_states((StateSet) (this.get_states().clone()));
		fsa.set_final_states((StateSet) (this.get_final_states().clone()));
		fsa.set_start_state(this.get_start_state());
		fsa.set_transitions((Transitions) (this.get_transitions().clone()));
		fsa.set_next_unused_state(this.get_next_unused_state());
		return fsa;
	}

	public static Fsa negates(Fsa fsa, Alphabet new_alphabet)
			throws NegateException {
		if (!fsa.is_deterministic()) {
			throw new NegateException("Negating a non-deterministic automata");
		}

		Fsa fsa_bar = (Fsa) (fsa.clone());
		fsa_bar.set_alphabet(new_alphabet);

		/* compute the final states of the negation */
		State dummpy = fsa_bar.get_next_unused_state();
		fsa_bar.update_unused_state(dummpy);
		StateSet final_bar = StateSet.union(StateSet.minus(
				fsa_bar.get_states(), fsa_bar.get_final_states()), StateSet
				.singleton(dummpy));
		fsa_bar.set_final_states(final_bar);

		java.util.Iterator is = fsa_bar.get_states().iterator();
		while (is.hasNext()) {
			State s = (State) (is.next());
			java.util.Iterator ia = new_alphabet.iterator();
			while (ia.hasNext()) {
				Label l = (Label) (ia.next());
				StateSet ss = fsa_bar.get_dest_states(s, l);
				if (ss == null) {
					fsa_bar.add_transition(s, l, dummpy);
				}
			}
		}
		return fsa_bar;
	}

	public String toString() {		
		String str = new String();
		 str = "States: " + states.toString() + "\n";
		 str += "Alphabets: " + alphabet.toString() + "\n";
		 str += "Start State: " + start_state.toString() + "\n";
		 str += "Final State: " + final_states.toString() + "\n";
		 //System.out.println("----" + str);
		str = "Transitions: \n" + t.toString() + "\n";
		return str;
	}
	
	public String toStringWeb() {
		String str = new String();
		// str = "States: " + states.toString() + "\n";
		// str += "Alphabets: " + alphabet.toString() + "\n";
		// str += "Start State: " + start_state.toString() + "\n";
		// str += "Final State: " + final_states.toString() + "\n";
		str = "Transitions: <br>" + t.toString() + "<br>";
		return str;
	}
}
